﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using SimpleIR;
using System.Diagnostics.Contracts;

namespace RgnAnalyzer.Domain
{
	/// <summary>
	/// A map from field names to the values that they contain implemented as a library that works on sorted arrays 
	/// of <c>APossiblePointerTargets</c>. We do it this way to avoid creating a class that is just a wrapper of an array.
	/// </summary>
	internal struct APtrValueMap
	{
		internal static APossiblePointerTarget[] EmptyTargetMap = new APossiblePointerTarget[0];

		internal static IRBasicAccessPath[] EmptyMayNullMap = new IRBasicAccessPath[0];

		internal static IRBasicAccessPath[] InitialPtrMayNullMap = new IRBasicAccessPath[] { IRBasicAccessPath.EmptyAccessPath };

		/// <summary>
		/// Array with all the possible pointer targets
		/// </summary>
		private readonly APossiblePointerTarget[] m_ptrinfo;

		/// <summary>
		/// Array containing all of the storage locations that may contain null pointers.
		/// May not synch exactly with ptrinfo as a result of clearing infeasible info.
		/// From the domain perspective we check if path not in here AND has an entry in ptrinfo for nullity tests.
		/// </summary>
		private readonly IRBasicAccessPath[] m_maynull;

		private APtrValueMap(APossiblePointerTarget[] ppa, IRBasicAccessPath[] maynullinfo)
		{
			Contract.Requires(ppa != null);
			Contract.Requires((ppa.Length != 0) | (ppa == EmptyTargetMap), "Hmm, something went wrong.");
			Contract.Requires((maynullinfo.Length != 0) | (maynullinfo == EmptyMayNullMap), "Hmm, something went wrong.");
			
			this.m_ptrinfo = ppa;
			this.m_maynull = maynullinfo;
		}

		internal static APtrValueMap MakeInitalPtrValueMapPtr()
		{
			return new APtrValueMap(EmptyTargetMap, InitialPtrMayNullMap);
		}

		internal static APtrValueMap MakeInitalPtrValueMapComposite(List<IRBasicAccessPath> allterminalaccp)
		{
			int ppt = allterminalaccp.Count((IRBasicAccessPath bap) => bap.PathLast.FieldType is IRPtrType);
			if(ppt == 0)
				return new APtrValueMap(EmptyTargetMap, EmptyMayNullMap);
			else
			{
				IRBasicAccessPath[] nullpp = new IRBasicAccessPath[ppt];
				int pos = 0;
				for(int i = 0; i < allterminalaccp.Count; ++i)
				{
					IRBasicAccessPath bb = allterminalaccp[i];

					if(bb.PathLast.FieldType is IRPtrType)
					{
						nullpp[pos] = bb;
						++pos;
					}
				}
				Array.Sort(nullpp);

				return new APtrValueMap(EmptyTargetMap, nullpp);
			}
		}

		internal static APtrValueMap MakePtrWSingleTarget(APossiblePointerTarget pp, bool mustnonnull)
		{
			Contract.Requires(pp.SourceOffset.IsEmptyAccessPath);

			IRBasicAccessPath[] nullity;
			if(mustnonnull)
				nullity = EmptyMayNullMap;
			else
				nullity = new IRBasicAccessPath[] { IRBasicAccessPath.EmptyAccessPath };	

			APossiblePointerTarget[] appta = new APossiblePointerTarget[] { pp };

			return new APtrValueMap(appta, nullity);
		}

		internal static APtrValueMap MakePtrPostCheckIsInst(APossiblePointerTarget[] app)
		{
			IRBasicAccessPath[] nullity;
			if(app.Length != 0)
				nullity = EmptyMayNullMap;
			else
				nullity = new IRBasicAccessPath[] { IRBasicAccessPath.EmptyAccessPath };

			return new APtrValueMap(app, nullity);
		}

		public override string ToString()
		{
			StringBuilder fmap = new StringBuilder("(");
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
			{
				if(i != 0)
					fmap.Append(", ");

				int nnpos = Array.BinarySearch(this.m_maynull, this.m_ptrinfo[i].SourceOffset);
				if(nnpos >= 0)
					fmap.Append("!");

				fmap.Append(this.m_ptrinfo[i].ToString());
			}
			fmap.Append(")");
			return fmap.ToString();
		}

		internal void CheckConsistent(IRType ltype, bool optcempty)
		{
			if(ltype is IRPtrType || ltype is IRReferenceType)
			{
				if(this.m_ptrinfo.Length == 0 && this.m_maynull.Length == 0)
					DebugReport.ReportError("Ptr has no targets but is marked as being non-null??");
			}
			else if(ltype is IRClassType)
			{
				foreach(IRBasicAccessPath bap in ltype.TypeDescription.AllTerminalAccessPaths)
				{
					if(!(bap.PathLast.FieldType is IRPtrType))
						continue;

					if(bap.AccessPathHasSummaryLocation && optcempty)
						continue;

					if(!this.m_ptrinfo.Any((APossiblePointerTarget ppt) => ppt.SourceOffset == bap) && !this.m_maynull.Contains(bap))
						DebugReport.ReportError("Ptr has no targets but is marked as being non-null??");
				}
			}
			else
			{ ;}
		}

		/// <summary>
		/// Return the number of possible pointer targets.
		/// </summary>
		internal int PTargetCount
		{ get { return this.m_ptrinfo.Length; } }

		/// <summary>
		/// Array with all the possible pointer targets
		/// </summary>
		internal APossiblePointerTarget[] PTargets
		{ get { return this.m_ptrinfo; } }

		/// <summary>
		/// Return true if the given location is known to be nonnull.
		/// </summary>
		internal bool PathMustNonNull(IRBasicAccessPath bap)
		{ return Array.BinarySearch(this.m_maynull, bap) < 0; }

		/// <summary>
		/// Read values from all prefix fields.
		/// Assume we are placing the results into a unqiue memory location.
		/// </summary>
		internal APtrValueMap ReadPtrValues(IRBasicAccessPath loc)
		{
			List<APossiblePointerTarget> appt = new List<APossiblePointerTarget>();
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
			{
				if(loc.IsAccessPathPrefixOf(this.m_ptrinfo[i].SourceOffset))
				{
					IRBasicAccessPath suffixpath = GlobalAnalysisState.TProg.GetAccessPathTailK(this.m_ptrinfo[i].SourceOffset, loc.Path.Length);
					APossiblePointerTarget rpp = this.m_ptrinfo[i].UpdateSourceOffset(suffixpath);

					int pos = appt.BinarySearch(rpp);
					if(pos < 0)
						appt.Insert(~pos, rpp.SetInjectivity(true));
					else
						appt[pos] = appt[pos].MergeOtherPointerTargetWith(rpp, false, true);
				}
			}

			List<IRBasicAccessPath> mnn = new List<IRBasicAccessPath>();
			for(int i = 0; i < this.m_maynull.Length; ++i)
			{
				if(loc.IsAccessPathPrefixOf(this.m_maynull[i]))
				{
					IRBasicAccessPath suffixpath = GlobalAnalysisState.TProg.GetAccessPathTailK(this.m_maynull[i], loc.Path.Length);
					
					int npos = mnn.BinarySearch(suffixpath);
					if(npos < 0)
						mnn.Insert(~npos, suffixpath);
				}
			}

			return new APtrValueMap(appt.Count == 0 ? EmptyTargetMap : appt.ToArray(), mnn.Count == 0 ? EmptyMayNullMap : mnn.ToArray());
		}

		/// <summary>
		/// Write values to all prefix fields.
		/// </summary>
		/// <param name="strongupdateok">True if we can strongly update the location that is written to.</param>
		/// <param name="intouniquelocation">True if the location is unique (vs. summary) location.</param>
		internal APtrValueMap WritePtrValues(APtrValueMap opvm, IRBasicAccessPath loc, bool strongupdateok, bool intouniquelocation)
		{
			Contract.Requires(loc != null);

			List<IRBasicAccessPath> nullp = new List<IRBasicAccessPath>();
			List<APossiblePointerTarget> intol = new List<APossiblePointerTarget>();

			//remove any pointer values as allowed by strong updates
			if(!strongupdateok)
			{
				nullp.AddRange(this.m_maynull);
				intol.AddRange(this.m_ptrinfo);
			}
			else
			{
				for(int i = 0; i < this.m_maynull.Length; ++i)
				{
					if((!loc.IsAccessPathPrefixOf(this.m_maynull[i])) || this.m_maynull[i].AccessPathHasSummaryLocation)
						nullp.Add(this.m_maynull[i]);
				}

				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
				{
					if((!loc.IsAccessPathPrefixOf(this.m_ptrinfo[i].SourceOffset)) || this.m_ptrinfo[i].SourceOffset.AccessPathHasSummaryLocation)
						intol.Add(this.m_ptrinfo[i]);
				}
			}

			//merge in the new pointers as possible
			int nsize = nullp.Count;
			for(int i = 0; i < opvm.m_maynull.Length; ++i)
			{
				IRBasicAccessPath wp = GlobalAnalysisState.TProg.GetAccessPathExtensionPost_WPath(loc, opvm.m_maynull[i]);
				
				int pos = nullp.BinarySearch(0, nsize, wp, null);
				if(pos < 0)
					nullp.Add(wp);
			}

			int osize = intol.Count;
			for(int i = 0; i < opvm.m_ptrinfo.Length; ++i)
			{
				IRBasicAccessPath wp = GlobalAnalysisState.TProg.GetAccessPathExtensionPost_WPath(loc, opvm.m_ptrinfo[i].SourceOffset);
				APossiblePointerTarget wpp = opvm.m_ptrinfo[i].UpdateSourceOffset(wp);

				int pos = intol.BinarySearch(0, osize, wpp, null);
				if(pos < 0)
					intol.Add(wpp);
				else
				{
					bool isuniqueloc = (intouniquelocation & (!wp.AccessPathHasSummaryLocation));
					intol[pos] = intol[pos].MergeOtherPointerTargetWith(wpp, false, isuniqueloc);
				}
			}

			IRBasicAccessPath[] nullpa;
			if(nullp.Count == 0)
				nullpa = EmptyMayNullMap;
			else
			{
				nullp.Sort();
				nullpa = nullp.ToArray();
			}

			APossiblePointerTarget[] appa;
			if(intol.Count == 0)
				appa = EmptyTargetMap;
			else
			{
				intol.Sort();
				appa = intol.ToArray();
			}

			return new APtrValueMap(appa, nullpa);
		}

		/// <summary>
		/// Write values to all prefix fields.
		/// </summary>
		/// <param name="strongupdateok">True if we can strongly update the location that is written to.</param>
		/// <param name="intouniquelocation">True if the location is unique (vs. summary) location.</param>
		internal APtrValueMap WritePtrValuesContainerBI(APtrValueMap opvm, IRBasicAccessPath loc, bool strongupdateok, IRMemberField knowninjfield)
		{
			Contract.Requires(loc != null);
			Contract.Requires(loc.AccessPathHasSummaryLocation);

			List<IRBasicAccessPath> nullp = new List<IRBasicAccessPath>();
			List<APossiblePointerTarget> intol = new List<APossiblePointerTarget>();

			//remove any pointer values as allowed by strong updates
			if(!strongupdateok)
			{
				nullp.AddRange(this.m_maynull);
				intol.AddRange(this.m_ptrinfo);
			}
			else
			{
				for(int i = 0; i < this.m_maynull.Length; ++i)
				{
					if((!loc.IsAccessPathPrefixOf(this.m_maynull[i])) || this.m_maynull[i].AccessPathHasSummaryLocation)
						nullp.Add(this.m_maynull[i]);
				}

				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
				{
					if((!loc.IsAccessPathPrefixOf(this.m_ptrinfo[i].SourceOffset)) || this.m_ptrinfo[i].SourceOffset.AccessPathHasSummaryLocation)
						intol.Add(this.m_ptrinfo[i]);
				}
			}

			//merge in the new pointers as possible
			int nsize = nullp.Count;
			for(int i = 0; i < opvm.m_maynull.Length; ++i)
			{
				IRBasicAccessPath wp = GlobalAnalysisState.TProg.GetAccessPathExtensionPost_WPath(loc, opvm.m_maynull[i]);

				int pos = nullp.BinarySearch(0, nsize, wp, null);
				if(pos < 0)
					nullp.Add(wp);
			}

			int osize = intol.Count;
			for(int i = 0; i < opvm.m_ptrinfo.Length; ++i)
			{
				IRBasicAccessPath wp = GlobalAnalysisState.TProg.GetAccessPathExtensionPost_WPath(loc, opvm.m_ptrinfo[i].SourceOffset);
				APossiblePointerTarget wpp = opvm.m_ptrinfo[i].UpdateSourceOffset(wp);

				int pos = intol.BinarySearch(0, osize, wpp, null);
				if(pos < 0)
					intol.Add(wpp);
				else
				{
					bool noaliasing = (knowninjfield == wp.PathLast);
					intol[pos] = intol[pos].MergeOtherPointerTargetWith(wpp, noaliasing, false);
				}
			}

			IRBasicAccessPath[] nullpa;
			if(nullp.Count == 0)
				nullpa = EmptyMayNullMap;
			else
			{
				nullp.Sort();
				nullpa = nullp.ToArray();
			}

			APossiblePointerTarget[] appa;
			if(intol.Count == 0)
				appa = EmptyTargetMap;
			else
			{
				intol.Sort();
				appa = intol.ToArray();
			}

			return new APtrValueMap(appa, nullpa);
		}

		/// <summary>
		/// Return the <c>ZeroOne.Value</c> encoding of the result of testing the two pointers for equality
		/// </summary>
		internal static ZeroOne.Value PointerEqualsTest(APtrValueMap p1, APtrValueMap p2)
		{
			if(p1.m_ptrinfo == EmptyTargetMap & p2.m_ptrinfo == EmptyTargetMap)
				return ZeroOne.Value.One;
			else if(p1.m_ptrinfo == EmptyTargetMap)
				return (p2.m_maynull.Length != 0) ? ZeroOne.Value.Unknown : ZeroOne.Value.Zero;
			else if(p2.m_ptrinfo == EmptyTargetMap)
				return (p1.m_maynull.Length != 0) ? ZeroOne.Value.Unknown : ZeroOne.Value.Zero;
			else
				return ZeroOne.Value.Unknown;
		}

		/// <summary>
		/// Return the <c>ZeroOne.Value</c> encoding of the result of testing the pointer for nullity
		/// </summary>
		internal ZeroOne.Value PointerNullTest()
		{
			if(this.m_ptrinfo == EmptyTargetMap)
				return ZeroOne.Value.One;
			else if(this.m_maynull.Length != 0)
				return ZeroOne.Value.Unknown; 
			else
				return ZeroOne.Value.Zero;
		}

		internal APtrValueMap AssertTargetNonNull()
		{ return new APtrValueMap(this.m_ptrinfo, EmptyMayNullMap); }

		/// <summary>
		/// Given an <c>ATrgtEnum</c> return the <c>APossiblePointerTarget</c> associated with it.
		/// </summary>
		internal APossiblePointerTarget ResolvePtrFromEnum(ATrgtEnum tenum)
		{ return this.m_ptrinfo[tenum.PosKey]; }

		/// <summary>
		/// Get an enumerator for the Pointer targets stored in this.
		/// </summary>
		public IEnumerator<ATrgtEnum> GetATrgtEnumerator()
		{ return new PTEnumerator(this.m_ptrinfo); }

		/// <summary>
		/// The enumerator we have to produce the targets in this.
		/// </summary>
		internal sealed class PTEnumerator : IEnumerator<ATrgtEnum>
		{
			private readonly APossiblePointerTarget[] m_ptr;
			private int m_rpos;

			internal PTEnumerator(APossiblePointerTarget[] tptr)
			{
				this.m_ptr = tptr;
				this.m_rpos = -1;
			}

			public ATrgtEnum Current
			{ get { return new ATrgtEnum(this.m_rpos, this.m_ptr[this.m_rpos]); } }

			public void Dispose()
			{ ;}

			object System.Collections.IEnumerator.Current
			{ get { return new ATrgtEnum(this.m_rpos, this.m_ptr[this.m_rpos]); } }

			public bool MoveNext()
			{
				if(this.m_rpos == this.m_ptr.Length)
					return false;

				++this.m_rpos;
				return this.m_rpos < this.m_ptr.Length;
			}

			public void Reset()
			{ this.m_rpos = -1; }
		}

		/// <summary>
		/// Return true if the two arrays of pointer targets are the same (in the abstract sense).
		/// BUT WE ASSUME TARGET CONSISTENCY IS DONE IN THE EXTERNAL ISOMORPHISM CODE.
		/// </summary>
		internal static bool DomainEqualIgnoreTargets(APtrValueMap lm1, APtrValueMap lm2)
		{
			if(lm1.m_maynull.Length != lm2.m_maynull.Length)
				return false;

			if(lm1.m_ptrinfo.Length != lm2.m_ptrinfo.Length)
				return false;

			for(int j = 0; j < lm1.m_maynull.Length; ++j)
			{
				if(lm1.m_maynull[j] != lm2.m_maynull[j])
					return false;
			}

			//Compute hash of ptr sets and compare. This allows us to discard obviously bad choices while 
			//exact equality checks will be done in isomorphism code
			int lm1hash = 0;
			int lm2hash = 0;
			int len = lm1.m_ptrinfo.Length;
			for(int i = 0; i < len; ++i)
			{
				lm1hash += lm1.m_ptrinfo[i].IsInjective ? 1 : 0;
				lm2hash += lm2.m_ptrinfo[i].IsInjective ? 1 : 0;
			}

			return lm1hash == lm2hash;
		}

		/// <summary>
		/// Merge the contents of two values (they are always compatible) and return the merged contents.
		/// </summary>
		/// <param name="noaliasingbetween">True if we have pointers that we know cannot be pairwise aliases (eg. do updates on the injectivity based on pairwise properties).</param>
		/// <param name="intouniquelocation">True if the merged values are into a unique (vs. summary) location.</param>
		internal static APtrValueMap MergeAPtrMaps(APtrValueMap pm1, APtrValueMap pm2, bool noaliasingbetween, bool intouniquelocation)
		{
			IRBasicAccessPath[] resnullity;
			if((pm1.m_maynull == EmptyMayNullMap) & (pm2.m_maynull == EmptyMayNullMap))
				resnullity = EmptyMayNullMap;
			else
			{
				List<IRBasicAccessPath> nntl = new List<IRBasicAccessPath>(pm1.m_maynull);

				int nsize = nntl.Count;
				for(int i = 0; i < pm2.m_maynull.Length; ++i)
				{
					IRBasicAccessPath bb = pm2.m_maynull[i];
					int pos = nntl.BinarySearch(0, nsize, bb, null);
					if(pos < 0)
						nntl.Add(bb);
				}

				nntl.Sort();
				resnullity = nntl.ToArray();
			}

			APossiblePointerTarget[] resapp;
			if((pm1.m_ptrinfo == EmptyTargetMap) & (pm2.m_ptrinfo == EmptyTargetMap))
				resapp = EmptyTargetMap;
			else
			{
				List<APossiblePointerTarget> pptl = new List<APossiblePointerTarget>(pm1.m_ptrinfo);

				int osize = pptl.Count;
				for(int i = 0; i < pm2.m_ptrinfo.Length; ++i)
				{
					APossiblePointerTarget pp = pm2.m_ptrinfo[i];
					int pos = pptl.BinarySearch(0, osize, pp, null);
					if(pos < 0)
						pptl.Add(pp);
					else
					{
						bool isuniqueloc = (intouniquelocation & (!pp.SourceOffset.AccessPathHasSummaryLocation));
						pptl[pos] = pptl[pos].MergeOtherPointerTargetWith(pp, noaliasingbetween, isuniqueloc);
					}
				}

				pptl.Sort();
				resapp = pptl.ToArray();
			}

			return new APtrValueMap(resapp, resnullity);
		}

		/// <summary>
		/// Initialize the loops index info
		/// </summary>
		internal APtrValueMap InitializeLoopPositionInfoAs(AIndexPosition.Value pos, IRBasicAccessPath okcontbap, IRBasicAccessPath okkeybap, IRBasicAccessPath okvalbap)
		{
			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				APossiblePointerTarget[] nppl = new APossiblePointerTarget[this.m_ptrinfo.Length];
				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
				{
					if((this.m_ptrinfo[i].SourceOffset == okcontbap) | (this.m_ptrinfo[i].SourceOffset == okkeybap) | (this.m_ptrinfo[i].SourceOffset == okvalbap))
						nppl[i] = this.m_ptrinfo[i].InitializeLoopPositionInfoAs(pos);
					else
						nppl[i] = this.m_ptrinfo[i];
				}

				return new APtrValueMap(nppl, this.m_maynull);
			}
		}

		/// <summary>
		/// return true if there is no loop info associated with any of the pointers here.
		/// </summary>
		internal bool HasLoopInfo()
		{
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
			{
				if(this.m_ptrinfo[i].IndexPosFlag != AIndexPosition.Value.Unknown)
					return true;
			}

			return false;
		}

		/// <summary>
		/// Advance the loop index info
		/// </summary>
		internal APtrValueMap AdvanceLoopPositionInfo()
		{
			Contract.Assert(this.m_ptrinfo != EmptyTargetMap);

			APossiblePointerTarget[] nppl = new APossiblePointerTarget[this.m_ptrinfo.Length];
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
				nppl[i] = this.m_ptrinfo[i].AdvanceLoopPositionInfo();

			return new APtrValueMap(nppl, this.m_maynull);
		}

		/// <summary>
		/// Clear all loop index info
		/// </summary>
		internal APtrValueMap ClearLoopPositionInfo()
		{
			Contract.Assert(this.m_ptrinfo != EmptyTargetMap);

			APossiblePointerTarget[] nppl = new APossiblePointerTarget[this.m_ptrinfo.Length];
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
				nppl[i] = this.m_ptrinfo[i].ClearLoopPositionInfo();
			return new APtrValueMap(nppl, this.m_maynull);
		}

		/// <summary>
		/// Mark all the possible pointers are being injective.
		/// </summary>
		internal APtrValueMap SetAllAsInjectiveAsNeededForUniqueLocation(IRType loctype)
		{
			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				APossiblePointerTarget[] nppl = new APossiblePointerTarget[this.m_ptrinfo.Length];
				if(loctype is IRDictionaryType)
				{
					IRMemberField contf = ((IRDictionaryType)loctype).ContentsField;
					IRMemberField keyf = ((IRKeyValuePairType)contf.FieldType).KeyField;
					for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					{
						IRBasicAccessPath pp = this.m_ptrinfo[i].SourceOffset;
						if(pp.Path.Length == 2 && ((pp.Path[0] == contf) & (pp.Path[1] == keyf)))
							nppl[i] = this.m_ptrinfo[i].SetInjectivity(true);
						else
							nppl[i] = this.m_ptrinfo[i];
					}
				}
				else if(loctype is IRContainerType)
				{
					if(loctype is IRDictionaryType)
					{
						IRMemberField dctk = ((IRKeyValuePairType)((IRDictionaryType)loctype).ContainerContentsType).KeyField;
						for(int i = 0; i < this.m_ptrinfo.Length; ++i)
						{
							if(dctk.FieldType is IRPtrType && this.m_ptrinfo[i].SourceOffset.PathLast == dctk)
								nppl[i] = this.m_ptrinfo[i].SetInjectivity(true);
							else
								nppl[i] = this.m_ptrinfo[i];
						}
					}
					else if(((IRContainerType)loctype).IsSetBehaviorContainer)
					{
						for(int i = 0; i < this.m_ptrinfo.Length; ++i)
							nppl[i] = this.m_ptrinfo[i].SetInjectivity(true);
					}
					else
					{
						for(int i = 0; i < this.m_ptrinfo.Length; ++i)
							nppl[i] = this.m_ptrinfo[i];
					}
				}
				else
				{
					for(int i = 0; i < this.m_ptrinfo.Length; ++i)
						nppl[i] = this.m_ptrinfo[i].SetInjectivity(true);
				}
				return new APtrValueMap(nppl, this.m_maynull);
			}
		}

		/// <summary>
		/// We may end up with an edge representing infeasible pointers so just eliminate the edge.
		/// </summary>
		internal APtrValueMap ScrubInfeasibleRef(ATrgtEnum trgte)
		{
			List<APossiblePointerTarget> nppl = new List<APossiblePointerTarget>();
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
			{
				if(i != trgte.PosKey)
					nppl.Add(this.m_ptrinfo[i]);
			}

			List<IRBasicAccessPath> mnl = new List<IRBasicAccessPath>(this.m_maynull);
			if(!nppl.Exists((APossiblePointerTarget apt) => apt.SourceOffset == trgte.BAPPath))
			{
				int ppos = mnl.BinarySearch(trgte.BAPPath);
				if(ppos < 0)
					mnl.Insert(~ppos, trgte.BAPPath);
			}

			APossiblePointerTarget[] ppa;
			if(nppl.Count == 0)
				ppa = EmptyTargetMap;
			else
				ppa = nppl.ToArray();

			IRBasicAccessPath[] mna;
			if(mnl.Count == 0)
				mna = EmptyMayNullMap;
			else
				mna = mnl.ToArray();

			return new APtrValueMap(ppa, mna);
		}

		/// <summary>
		/// After analyzing a recursive call we may have some infeasible locations, so delete these addresses.
		/// </summary>
		internal APtrValueMap DeletePossibleTargets(HashSet<int> deleteset)
		{
			Contract.Requires(deleteset != null);

			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				List<APossiblePointerTarget> nppl = new List<APossiblePointerTarget>();
				HashSet<IRBasicAccessPath> delpaths = new HashSet<IRBasicAccessPath>();

				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
				{
					if(!deleteset.Contains(this.m_ptrinfo[i].PTarget))
						nppl.Add(this.m_ptrinfo[i]);
					else
						delpaths.Add(this.m_ptrinfo[i].SourceOffset);
				}

				List<IRBasicAccessPath> mnl = new List<IRBasicAccessPath>(this.m_maynull);
				foreach(IRBasicAccessPath delp in delpaths)
				{
					if(!nppl.Exists((APossiblePointerTarget apt) => apt.SourceOffset == delp))
					{
						int ppos = mnl.BinarySearch(delp);
						if(ppos < 0)
							mnl.Insert(~ppos, delp);
					}
				}

				APossiblePointerTarget[] ppa;
				if(nppl.Count == 0)
					ppa = EmptyTargetMap;
				else
					ppa = nppl.ToArray();

				IRBasicAccessPath[] mna;
				if(mnl.Count == 0)
					mna = EmptyMayNullMap;
				else
					mna = mnl.ToArray();

				return new APtrValueMap(ppa, mna);
			}
		}

		/// <summary>
		/// During compaction after removing unreachable locations we update the addresses in the pointers.
		/// </summary>
		internal APtrValueMap UpdateAddresses_ISOMapping(Dictionary<int, int> addrReMap)
		{
			Contract.Requires(addrReMap != null);

			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				APossiblePointerTarget[] upp = new APossiblePointerTarget[this.m_ptrinfo.Length];
				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					upp[i] = this.m_ptrinfo[i].UpdateTargetValue(addrReMap[this.m_ptrinfo[i].PTarget]);

				Array.Sort(upp);
				return new APtrValueMap(upp, this.m_maynull);
			}
		}

		/// <summary>
		/// On normal form computation we merge equivalence classes from locations on the same flow history use this to replace old address sets with new sets.
		/// Has control for if this in a unique location (and always assumes that pointers which get merged are pairwise non-aliased).
		/// </summary>
		/// <param name="intouniquelocation">True if the merged values are into a unique (vs. summary) location.</param>
		internal APtrValueMap UpdatedAddresses_MayMergeButNoNewInj(Dictionary<int, int> addrReMap, bool intouniquelocation)
		{
			Contract.Requires(addrReMap != null);

			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				List<APossiblePointerTarget> nppl = new List<APossiblePointerTarget>();
				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					nppl.Add(this.m_ptrinfo[i].UpdateTargetValue(addrReMap[this.m_ptrinfo[i].PTarget]));
				nppl.Sort();

				int cpos = 0;
				for(int i = 1; i < nppl.Count; ++i)
				{
					APossiblePointerTarget pp = nppl[i];

					if(pp != nppl[cpos])
					{
						++cpos;
						nppl[cpos] = nppl[i];
					}
					else
					{
						bool isuniqueloc = (intouniquelocation & (!pp.SourceOffset.AccessPathHasSummaryLocation));
						nppl[cpos] = nppl[cpos].MergeOtherPointerTargetWith(pp, true, isuniqueloc);
					}
				}

				nppl.RemoveRange(cpos + 1, nppl.Count - (cpos + 1));
				return new APtrValueMap(nppl.ToArray(), this.m_maynull);
			}
		}

		/// <summary>
		/// Return true if this ptr may have a target in the given set of addresses.
		/// </summary>
		internal bool HasTargetInSet(HashSet<int> targetset)
		{
			for(int i = 0; i < this.m_ptrinfo.Length; ++i)
			{
				if(targetset.Contains(this.m_ptrinfo[i].PTarget))
					return true;
			}

			return false;
		}

		/// <summary>
		/// When introducing cutpoints replace and cross addresses with the cutpoint id (in the unreach section) for later patching.
		/// </summary>
		internal APtrValueMap ReplaceAssociatedCutpointsAsNeeded(Dictionary<int, int> addressToCPIDMap)
		{
			Contract.Requires(addressToCPIDMap != null);

			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				bool repl = false;
				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					repl |= addressToCPIDMap.ContainsKey(this.m_ptrinfo[i].PTarget);

				APossiblePointerTarget[] nrra;
				if(!repl)
					nrra = this.m_ptrinfo;
				else
				{
					nrra = new APossiblePointerTarget[this.m_ptrinfo.Length];
					for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					{
						int mrv = this.m_ptrinfo[i].PTarget;
						if(addressToCPIDMap.ContainsKey(mrv))
							nrra[i] = this.m_ptrinfo[i].UpdateTargetValue(addressToCPIDMap[mrv]);
						else
							nrra[i] = this.m_ptrinfo[i];
					}
					Array.Sort(nrra);
				}

				return new APtrValueMap(nrra, this.m_maynull);
			}
		}

		/// <summary>
		/// Replace the cutpoint ids with the approapriate target location addresses.
		/// </summary>
		/// <param name="intouniquelocation">True if the values are in a unique (vs. summary) location.</param>
		internal APtrValueMap UpdateOutEdgesAfterCutpointEdgeExpand(Dictionary<int, int[]> cpidToAddressMap, bool intouniquelocation)
		{
			Contract.Requires(cpidToAddressMap != null);

			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);
			else
			{
				bool hasexpand = false;
				for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					hasexpand |= cpidToAddressMap.ContainsKey(this.m_ptrinfo[i].PTarget);

				if(!hasexpand)
					return new APtrValueMap(this.m_ptrinfo, this.m_maynull);
				else
				{
					List<APossiblePointerTarget> nppl = new List<APossiblePointerTarget>();
					for(int i = 0; i < this.m_ptrinfo.Length; ++i)
					{
						if(!cpidToAddressMap.ContainsKey(this.m_ptrinfo[i].PTarget))
							nppl.Add(this.m_ptrinfo[i]);
						else
						{
							int[] rma = cpidToAddressMap[this.m_ptrinfo[i].PTarget];
							for(int j = 0; j < rma.Length; ++j)
								nppl.Add(this.m_ptrinfo[i].UpdateTargetValue(rma[j]));
						}
					}

					int cpos = 0;
					for(int i = 1; i < nppl.Count; ++i)
					{
						APossiblePointerTarget pp = nppl[i];

						if(pp != nppl[cpos])
						{
							++cpos;
							nppl[cpos] = nppl[i];
						}
						else
						{
							bool isuniqueloc = (intouniquelocation & (!pp.SourceOffset.AccessPathHasSummaryLocation));
							nppl[cpos] = nppl[cpos].MergeOtherPointerTargetWith(pp, true, isuniqueloc);
						}
					}

					nppl.RemoveRange(cpos + 1, nppl.Count - (cpos + 1));
					return new APtrValueMap(nppl.ToArray(), this.m_maynull);
				}
			}
		}

		internal APtrValueMap CopyWithLimitedTargetSet(ATrgtEnum oktrgt)
		{
			if(this.m_ptrinfo == EmptyTargetMap)
				return new APtrValueMap(EmptyTargetMap, this.m_maynull);

			APossiblePointerTarget aprt = this.m_ptrinfo[oktrgt.PosKey];
			APossiblePointerTarget[] appta = new APossiblePointerTarget[] { aprt };

			return new APtrValueMap(appta, this.m_maynull);
		}
	}

	/// <summary>
	/// Represents a possible pointer target.
	/// </summary>
	internal struct APossiblePointerTarget : IEquatable<APossiblePointerTarget>, IComparable<APossiblePointerTarget>
	{
		/// <summary>
		/// The offset of this pointer in the source location where it is stored.
		/// </summary>
		internal readonly IRBasicAccessPath SourceOffset;

		/// <summary>
		/// The target address
		/// </summary>
		internal readonly int PTarget;

		/// <summary>
		/// If the possible abstract pointer is injective
		/// </summary>
		internal readonly bool IsInjective;

		/// <summary>
		/// If it was derived from an array we are indexing on capture the info
		/// </summary>
		internal readonly AIndexPosition.Value IndexPosFlag;

		internal APossiblePointerTarget(IRBasicAccessPath source, int trgt, bool inj, AIndexPosition.Value ipo)
		{
			Contract.Requires(source != null);
			
			this.SourceOffset = source;
			this.PTarget = trgt;
			this.IsInjective = inj;
		
			this.IndexPosFlag = ipo;
		}

		/// <summary>
		/// Make a simple pointer target (injective and stored at the EmptyAccessPath).
		/// </summary>
		internal APossiblePointerTarget(int trgt)
		{
			this.SourceOffset = IRBasicAccessPath.EmptyAccessPath;
			this.PTarget = trgt;
			this.IsInjective = true;
		
			this.IndexPosFlag = AIndexPosition.Value.Unknown;
		}

		internal APossiblePointerTarget UpdateSourceOffset(IRBasicAccessPath newsource)
		{ return new APossiblePointerTarget(newsource, this.PTarget, this.IsInjective, this.IndexPosFlag); }

		internal APossiblePointerTarget UpdateTargetValue(int trgt)
		{ return new APossiblePointerTarget(this.SourceOffset, trgt, this.IsInjective, this.IndexPosFlag); }

		internal APossiblePointerTarget SetInjectivity(bool inj)
		{ return new APossiblePointerTarget(this.SourceOffset, this.PTarget, inj, this.IndexPosFlag); }

		internal APossiblePointerTarget InitializeLoopPositionInfoAs(AIndexPosition.Value pos)
		{ return new APossiblePointerTarget(this.SourceOffset, this.PTarget, this.IsInjective, pos); }

		internal APossiblePointerTarget AdvanceLoopPositionInfo()
		{ return new APossiblePointerTarget(this.SourceOffset, this.PTarget, this.IsInjective, AIndexPosition.AdvanceIndexPosition(this.IndexPosFlag)); }

		internal APossiblePointerTarget ClearLoopPositionInfo()
		{ return new APossiblePointerTarget(this.SourceOffset, this.PTarget, this.IsInjective, AIndexPosition.Value.Unknown); }

		/// <summary>
		/// Return true if the two edges are equal in the abstract doamin lattice sense.
		/// BUT WE ASSUME TARGET CONSISTENCY IS DONE IN THE EXTERNAL ISOMORPHISM CODE
		/// </summary>
		internal bool DomainEqualIgnoreTargetAddress(APossiblePointerTarget opt)
		{
			return (this.SourceOffset == opt.SourceOffset) & (this.IsInjective == opt.IsInjective) & (this.IndexPosFlag == opt.IndexPosFlag); 
		}

		/// <summary>
		/// Take two possible pointer targets to the same abstract address and merge their info.
		/// </summary>
		/// <param name="noaliasingbetween">True if we have pointers that we know cannot be pairwise aliases (eg. do updates on the injectivity based on pairwise properties).</param>
		/// <param name="intouniquelocation">True if the merged values are into a unique (vs. summary) location and thus are always injective.</param>
		internal APossiblePointerTarget MergeOtherPointerTargetWith(APossiblePointerTarget opt, bool noaliasingbetween, bool intouniquelocation)
		{
			Contract.Requires(this.SourceOffset == opt.SourceOffset);
			Contract.Requires(this.PTarget == opt.PTarget);

			AIndexPosition.Value ip = AIndexPosition.JoinPosition(this.IndexPosFlag, opt.IndexPosFlag);

			bool jinj;
			if(intouniquelocation)
				jinj = true;
			else
			{
				bool pinj = noaliasingbetween | AIndexPosition.PositionsGiveInjective(this.IndexPosFlag, opt.IndexPosFlag);
				jinj = this.IsInjective & opt.IsInjective & pinj;
			}

			return new APossiblePointerTarget(this.SourceOffset, this.PTarget, jinj, ip);
		}

		public override string ToString()
		{
			StringBuilder sb = new StringBuilder(this.PTarget + "(" + (this.IsInjective ? "Inj" : "Non"));
			
			if(this.IndexPosFlag != AIndexPosition.Value.Unknown)
				sb.Append(AIndexPosition.ConvertToString(this.IndexPosFlag));

			sb.Append(")");
			return sb.ToString();
		}

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public static bool operator ==(APossiblePointerTarget opt1, APossiblePointerTarget opt2)
		{ return opt1.Equals(opt2); }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public static bool operator !=(APossiblePointerTarget opt1, APossiblePointerTarget opt2)
		{ return !opt1.Equals(opt2); }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public static bool operator <(APossiblePointerTarget opt1, APossiblePointerTarget opt2)
		{ return opt1.CompareTo(opt2) < 0; }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public static bool operator >(APossiblePointerTarget opt1, APossiblePointerTarget opt2)
		{ return opt1.CompareTo(opt2) > 0; }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public override int GetHashCode()
		{ return this.SourceOffset.GetHashCode() ^ this.PTarget; }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public override bool Equals(Object obj)
		{ return (obj is APossiblePointerTarget) && this.Equals((APossiblePointerTarget)obj); }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public bool Equals(APossiblePointerTarget other)
		{ return (this.SourceOffset == other.SourceOffset) & (this.PTarget == other.PTarget); }

		/// <summary>
		/// ONLY ON TARGET!!
		/// </summary>
		public int CompareTo(APossiblePointerTarget other)
		{
			int cmpv = this.SourceOffset.CompareTo(other.SourceOffset);
			return (cmpv != 0) ? cmpv : (this.PTarget - other.PTarget); 
		}
	}
}
